ordinal(buchholz): Slice 3 umbrella extension — _<ᵇ¹_ with joint-bplus + strict-head dispatch#142
Merged
Merged
Conversation
…s constructor + dispatch
Extends `Ordinal.Buchholz.RankMonoUmbrella._<ᵇ⁰_` (10/13 closed
constructors) into a new `_<ᵇ¹_` adding a `<ᵇ¹-+1-+` constructor
for the joint-bplus case where the target's left summand is itself
a `bplus` (excluded by `_<ᵇ⁰_`'s atomic-target restriction).
The new constructor carries the strict-head premise `head-Ω x₁ <Ω
head-Ω y₁` plus WfCNF / NonBzero side conditions, and the umbrella
`rank-pow-mono-<ᵇ¹` dispatches it via Slice 3 headline
`rank-mono-<ᵇ-+1-via-head-Ω` from `RankPowSlice3Headline`.
Honest scope:
* The 10 inherited constructors forward to `rank-pow-mono-<ᵇ⁰`
via a thin `<ᵇ¹-from-<ᵇ⁰` embedding constructor (no
duplication).
* The strict-head sub-cases (x₁ = bOmega; x₁ = bpsi at strict
ν <Ω head-Ω y₁) discharge cleanly via the Slice 3 headline —
the caller's case-split on `x₁ <ᵇ y₁` derives the strict-head
premise via `head-Ω-inv-bOmega` (strict) or `head-Ω-inv-bpsi`
+ a strict refinement.
* The bpsi-source-at-equality sub-case (ν = head-Ω y₁) is
DOCUMENTED AS GATED rather than shipped broken: no rank-lex
primitive currently exists for `<ᵇ-+1` (the existing
`RankLex.rank-mono-<ᵇ-ψΩ≤-lex` only discharges `<ᵇ-ψΩ≤`).
When that primitive lands, a second constructor can be added
and the umbrella extended to dispatch on it.
Build + discipline:
* `--safe --without-K` throughout; no postulates, no funext.
* Wired into `proofs/agda/All.agda` adjacent to `RankMonoUmbrella`.
* Pinned in `proofs/agda/Ordinal/Buchholz/Smoke.agda` under its
own `using` block per CLAUDE.md "Working rules".
* `agda -i proofs/agda proofs/agda/All.agda` exits 0;
`agda -i proofs/agda proofs/agda/Smoke.agda` exits 0;
`agda -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agda`
exits 0; `bash scripts/kernel-guard.sh` PASS.
Headlines pinned:
* `_<ᵇ¹_`, `<ᵇ¹-from-<ᵇ⁰`, `<ᵇ¹-+1-+`, `rank-pow-mono-<ᵇ¹`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 74 issues detected
View findings[
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/echo-types/echo-types",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Issue in codeql.yml",
"type": "missing_workflow",
"file": "codeql.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "unknown",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "unknown",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "unknown",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "unknown",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
2 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 28, 2026
## Summary Two corrections to PR #144's narrative refresh. ## ResidueForm instance count: 6 → 8 PR #144 stated the post-#139 ResidueForm count as six. The actual count is eight. The pre-#139 baseline was already six (not four): the 2026-05-27 audit-follow-on landed \`indexed-residue\` + \`cost-residue\` (lines 181–234 of EchoResidueTaxonomy.agda). PR #139 then added \`search-residue\` + \`epistemic-residue\`, for a total of 8. ## Slice 3 closure: PRs #142 + #143 PR #144 framed the Slice 3 umbrella case-split as remaining work and the \`bpsi=bpsi at equal markers\` sub-case as still needing α's rank via rank-adm / rank-lex. Both landed in PRs #142 + #143: - **PR #142** — \`_<ᵇ¹_\` extension with joint-bplus + strict-head dispatch wires the headline (from #141) into the umbrella. - **PR #143** — \`bpsi-source-at-equality\` ψ-rank discharge closes the last sub-case via rank-lex. CHANGELOG + EXPLAINME updated to acknowledge both. ## Files - CHANGELOG.md — count fix + new Slice 3 follow-on bullet (#142 + #143) - EXPLAINME.adoc — Slice 3 narrative refreshed - docs/echo-types/MAP.adoc — 8 instances enumerated with landing dates - README.md — Tier 2 mermaid label - readme.adoc — Tier 2 list mirror ## Verification \`scripts/kernel-guard.sh\` PASS. No Agda code changed. ## Test plan - [x] kernel-guard.sh PASS - [ ] Admin-merge if budget permits Refs: echo-types#142, echo-types#143, echo-types#144. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 28, 2026
…ay's closed cases Ships the deliberately-narrowed `_<ᵇ⁻_` umbrella covering ALL CASES THAT CLOSE AT THE RANK-POW LEVEL TODAY: * 10 constructors via `_<ᵇ⁰_` inheritance (the `Ordinal.Buchholz.RankMonoUmbrella.rank-pow-mono-<ᵇ⁰` workhorse). * `<ᵇ-+1` joint-bplus UNDER STRICT HEAD via `_<ᵇ¹_-+1-+` (the Slice 3 closure landed in PR #142). New module `Ordinal.Buchholz.RankMonoUmbrellaSlice4`: * `_<ᵇ⁻ⁿ_` — narrowed WfCNF-restricted relation bundling source-WfCNF + target-WfCNF + `_<ᵇ¹_` derivation. * `<ᵇ⁻ⁿ-from-<ᵇ⁰`, `<ᵇ⁻ⁿ-+1-+` — constructor-level embeddings. * `rank-pow-mono-<ᵇ⁻ⁿ` — THE NARROWED UMBRELLA, forwards via `rank-pow-mono-<ᵇ¹`. * `<ᵇ⁻ⁿ-shortfall-{lex,equal-head}` — matched-negative `⊤`-aliases pinning the two `<ᵇ`-constructor-level shortfalls with explicit in-file pointers to where each closure lives (lex-rank level for `<ᵇ-ψΩ≤`; rank-lex-jb pivot for `<ᵇ-+1` at equal-head, PR #147 scaffold). Honest scope: this is the narrowed-but-real umbrella. The two shortfalls are not patched here; they are pinned as `grep`-able markers so the next session can extend the umbrella without re-deriving the analysis. The (a)+(b)+(c) assembly for the equal-head closure is the multi-PR follow-on documented in `RankLexJointBplus.agda`'s preamble. Wired into `All.agda` adjacent to `RankMonoUmbrellaSlice3`; pinned in `Ordinal/Buchholz/Smoke.agda` under own block per CLAUDE.md Working rules. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
RankMonoUmbrella._<ᵇ⁰_(10/13 closed constructors) into a new_<ᵇ¹_adding a<ᵇ¹-+1-+constructor for the joint-bplus case where the target's left summand is itself abplus(excluded by_<ᵇ⁰_'s atomic-target restriction).rank-pow-mono-<ᵇ¹dispatches inherited cases torank-pow-mono-<ᵇ⁰(via a thin<ᵇ¹-from-<ᵇ⁰embedding) and the new case to Slice 3 headlinerank-mono-<ᵇ-+1-via-head-ΩfromRankPowSlice3Headline.<ᵇ-+1-specific rank-lex primitive (the existingRankLex.rank-mono-<ᵇ-ψΩ≤-lexonly discharges<ᵇ-ψΩ≤).Files
proofs/agda/Ordinal/Buchholz/RankMonoUmbrellaSlice3.agda(114 lines).proofs/agda/All.agda(1 line, adjacent toRankMonoUmbrella).proofs/agda/Ordinal/Buchholz/Smoke.agda(ownusingblock per CLAUDE.md "Working rules").Headlines pinned:
_<ᵇ¹_,<ᵇ¹-from-<ᵇ⁰,<ᵇ¹-+1-+,rank-pow-mono-<ᵇ¹.Discipline
--safe --without-Kthroughout; no postulates, no funext.All.agda+ top-levelSmoke.agda+Ordinal/Buchholz/Smoke.agdaall exit 0.bash scripts/kernel-guard.shPASS.Test plan
agda -i proofs/agda proofs/agda/Ordinal/Buchholz/RankMonoUmbrellaSlice3.agdaexits 0agda -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agdaexits 0agda -i proofs/agda proofs/agda/Smoke.agdaexits 0agda -i proofs/agda proofs/agda/All.agdaexits 0bash scripts/kernel-guard.shPASSForward path
When a
<ᵇ-+1-specific rank-lex primitive lands (Route A fromRankPowSlice3design note), add a second constructor (e.g.,<ᵇ¹-+1-+-eq) carrying the rank-lex witness for the equality sub-case and extendrank-pow-mono-<ᵇ¹to dispatch on it. The current ship covers the strict-head subset cleanly without overclaim.